es:ES{i}, ff:FIFO{i:l}(es), is_req, is_ack:(E{i}), awaiting, owes_ack:(IdIdId).
(ff.C r Id)
 (i, j:ff.C. @i(awaiting(i,j):) & @i(owes_ack(i,j):))
 (i:ff.C, e:E. (ff.R(i,e))  (loc(e) = i  Id))
 (e:E. Dec(is_req(e)) & Dec(is_ack(e)))
 (i, j:ff.C, e:E. (ff.S(i,j,e))  (loc(e) = i  Id))
 (plus-ify{i:l}(es; ff; is_req; is_ack; awaiting; owes_ack)  {i'}) 

latex

Definitions	x:A. B(x), A c B, P  Q, [e: i p j], [e: i p j], plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack), t  T, P & Q, P  Q, , x:A. B(x), @i(x:T)
Lemmas	event system wf, FIFO wf, es-dtype wf, fifoR wf, decidable wf, es-loc wf, Id wf, fifoS wf, es-E wf, fifoC wf, es-causl wf, not wf, es-after wf, es-when wf, bool wf, es-vartype wf, es-initially wf